YES 0.849
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ LR
mainModule Main
| ((sequence :: Monad b => [b a] -> b [a]) :: Monad b => [b a] -> b [a]) |
module Main where
Lambda Reductions:
The following Lambda expression
\xs→return (x : xs)
is transformed to
sequence0 | x xs | = return (x : xs) |
The following Lambda expression
\x→sequence cs >>= sequence0 x
is transformed to
sequence1 | cs x | = sequence cs >>= sequence0 x |
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
mainModule Main
| ((sequence :: Monad a => [a b] -> a [b]) :: Monad a => [a b] -> a [b]) |
module Main where
Replaced joker patterns by fresh variables and removed binding patterns.
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule Main
| ((sequence :: Monad b => [b a] -> b [a]) :: Monad b => [b a] -> b [a]) |
module Main where
Cond Reductions:
The following Function with conditions
is transformed to
undefined0 | True | = undefined |
undefined1 | | = undefined0 False |
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
mainModule Main
| (sequence :: Monad a => [a b] -> a [b]) |
module Main where
Haskell To QDPs
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_psPs(:(vx90, vx91), vx4, ba) → new_psPs(vx91, vx4, ba)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_psPs(:(vx90, vx91), vx4, ba) → new_psPs(vx91, vx4, ba)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_gtGtEs(:(vx610, vx611), vx300, ba) → new_gtGtEs(vx611, vx300, ba)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_gtGtEs(:(vx610, vx611), vx300, ba) → new_gtGtEs(vx611, vx300, ba)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
new_gtGtEs0(:(vx300, vx301), vx31, ba) → new_psPs0(vx31, vx300, new_gtGtEs1(vx301, vx31, ba), ba)
new_sequence1(vx31, vx7, ba) → new_sequence(vx31, ty_IO, ba)
new_psPs0(vx31, vx300, vx4, ba) → new_sequence(vx31, ty_[], ba)
new_sequence(:(:(vx300, vx301), vx31), ty_[], ba) → new_gtGtEs0(vx301, vx31, ba)
new_gtGtEs0(:(vx300, vx301), vx31, ba) → new_gtGtEs0(vx301, vx31, ba)
new_sequence(:(:(vx300, vx301), vx31), ty_[], ba) → new_psPs0(vx31, vx300, new_gtGtEs1(vx301, vx31, ba), ba)
new_sequence(:(vx30, vx31), ty_IO, ba) → new_sequence(vx31, ty_IO, ba)
new_sequence(:(Just(vx300), vx31), ty_Maybe, ba) → new_sequence(vx31, ty_Maybe, ba)
The TRS R consists of the following rules:
new_psPs4([], vx4, ba) → vx4
new_gtGtEs1([], vx31, ba) → []
new_psPs2(vx31, vx300, vx4, ba) → new_psPs3(new_sequence0(vx31, ty_[], ba), vx300, vx4, ba)
new_psPs3([], vx300, vx4, ba) → new_psPs1(vx4, ba)
new_psPs1(vx4, ba) → vx4
new_psPs5(vx300, vx60, vx9, vx4, ba) → :(:(vx300, vx60), new_psPs4(vx9, vx4, ba))
new_gtGtEs2([], vx300, ba) → []
new_gtGtEs2(:(vx610, vx611), vx300, ba) → new_psPs4(:(:(vx300, vx610), []), new_gtGtEs2(vx611, vx300, ba), ba)
new_psPs4(:(vx90, vx91), vx4, ba) → :(vx90, new_psPs4(vx91, vx4, ba))
new_psPs3(:(vx60, vx61), vx300, vx4, ba) → new_psPs5(vx300, vx60, new_psPs1(new_gtGtEs2(vx61, vx300, ba), ba), vx4, ba)
new_gtGtEs1(:(vx300, vx301), vx31, ba) → new_psPs2(vx31, vx300, new_gtGtEs1(vx301, vx31, ba), ba)
The set Q consists of the following terms:
new_gtGtEs1(:(x0, x1), x2, x3)
new_gtGtEs2(:(x0, x1), x2, x3)
new_psPs5(x0, x1, x2, x3, x4)
new_psPs2(x0, x1, x2, x3)
new_gtGtEs2([], x0, x1)
new_psPs3(:(x0, x1), x2, x3, x4)
new_psPs4(:(x0, x1), x2, x3)
new_psPs3([], x0, x1, x2)
new_gtGtEs1([], x0, x1)
new_psPs1(x0, x1)
new_psPs4([], x0, x1)
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 3 SCCs with 1 less node.
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_sequence(:(Just(vx300), vx31), ty_Maybe, ba) → new_sequence(vx31, ty_Maybe, ba)
The TRS R consists of the following rules:
new_psPs4([], vx4, ba) → vx4
new_gtGtEs1([], vx31, ba) → []
new_psPs2(vx31, vx300, vx4, ba) → new_psPs3(new_sequence0(vx31, ty_[], ba), vx300, vx4, ba)
new_psPs3([], vx300, vx4, ba) → new_psPs1(vx4, ba)
new_psPs1(vx4, ba) → vx4
new_psPs5(vx300, vx60, vx9, vx4, ba) → :(:(vx300, vx60), new_psPs4(vx9, vx4, ba))
new_gtGtEs2([], vx300, ba) → []
new_gtGtEs2(:(vx610, vx611), vx300, ba) → new_psPs4(:(:(vx300, vx610), []), new_gtGtEs2(vx611, vx300, ba), ba)
new_psPs4(:(vx90, vx91), vx4, ba) → :(vx90, new_psPs4(vx91, vx4, ba))
new_psPs3(:(vx60, vx61), vx300, vx4, ba) → new_psPs5(vx300, vx60, new_psPs1(new_gtGtEs2(vx61, vx300, ba), ba), vx4, ba)
new_gtGtEs1(:(vx300, vx301), vx31, ba) → new_psPs2(vx31, vx300, new_gtGtEs1(vx301, vx31, ba), ba)
The set Q consists of the following terms:
new_gtGtEs1(:(x0, x1), x2, x3)
new_gtGtEs2(:(x0, x1), x2, x3)
new_psPs5(x0, x1, x2, x3, x4)
new_psPs2(x0, x1, x2, x3)
new_gtGtEs2([], x0, x1)
new_psPs3(:(x0, x1), x2, x3, x4)
new_psPs4(:(x0, x1), x2, x3)
new_psPs3([], x0, x1, x2)
new_gtGtEs1([], x0, x1)
new_psPs1(x0, x1)
new_psPs4([], x0, x1)
We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_sequence(:(Just(vx300), vx31), ty_Maybe, ba) → new_sequence(vx31, ty_Maybe, ba)
R is empty.
The set Q consists of the following terms:
new_gtGtEs1(:(x0, x1), x2, x3)
new_gtGtEs2(:(x0, x1), x2, x3)
new_psPs5(x0, x1, x2, x3, x4)
new_psPs2(x0, x1, x2, x3)
new_gtGtEs2([], x0, x1)
new_psPs3(:(x0, x1), x2, x3, x4)
new_psPs4(:(x0, x1), x2, x3)
new_psPs3([], x0, x1, x2)
new_gtGtEs1([], x0, x1)
new_psPs1(x0, x1)
new_psPs4([], x0, x1)
We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.
new_gtGtEs1(:(x0, x1), x2, x3)
new_gtGtEs2(:(x0, x1), x2, x3)
new_psPs5(x0, x1, x2, x3, x4)
new_psPs2(x0, x1, x2, x3)
new_gtGtEs2([], x0, x1)
new_psPs3(:(x0, x1), x2, x3, x4)
new_psPs4(:(x0, x1), x2, x3)
new_psPs3([], x0, x1, x2)
new_gtGtEs1([], x0, x1)
new_psPs1(x0, x1)
new_psPs4([], x0, x1)
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_sequence(:(Just(vx300), vx31), ty_Maybe, ba) → new_sequence(vx31, ty_Maybe, ba)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_sequence(:(Just(vx300), vx31), ty_Maybe, ba) → new_sequence(vx31, ty_Maybe, ba)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_sequence(:(vx30, vx31), ty_IO, ba) → new_sequence(vx31, ty_IO, ba)
The TRS R consists of the following rules:
new_psPs4([], vx4, ba) → vx4
new_gtGtEs1([], vx31, ba) → []
new_psPs2(vx31, vx300, vx4, ba) → new_psPs3(new_sequence0(vx31, ty_[], ba), vx300, vx4, ba)
new_psPs3([], vx300, vx4, ba) → new_psPs1(vx4, ba)
new_psPs1(vx4, ba) → vx4
new_psPs5(vx300, vx60, vx9, vx4, ba) → :(:(vx300, vx60), new_psPs4(vx9, vx4, ba))
new_gtGtEs2([], vx300, ba) → []
new_gtGtEs2(:(vx610, vx611), vx300, ba) → new_psPs4(:(:(vx300, vx610), []), new_gtGtEs2(vx611, vx300, ba), ba)
new_psPs4(:(vx90, vx91), vx4, ba) → :(vx90, new_psPs4(vx91, vx4, ba))
new_psPs3(:(vx60, vx61), vx300, vx4, ba) → new_psPs5(vx300, vx60, new_psPs1(new_gtGtEs2(vx61, vx300, ba), ba), vx4, ba)
new_gtGtEs1(:(vx300, vx301), vx31, ba) → new_psPs2(vx31, vx300, new_gtGtEs1(vx301, vx31, ba), ba)
The set Q consists of the following terms:
new_gtGtEs1(:(x0, x1), x2, x3)
new_gtGtEs2(:(x0, x1), x2, x3)
new_psPs5(x0, x1, x2, x3, x4)
new_psPs2(x0, x1, x2, x3)
new_gtGtEs2([], x0, x1)
new_psPs3(:(x0, x1), x2, x3, x4)
new_psPs4(:(x0, x1), x2, x3)
new_psPs3([], x0, x1, x2)
new_gtGtEs1([], x0, x1)
new_psPs1(x0, x1)
new_psPs4([], x0, x1)
We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_sequence(:(vx30, vx31), ty_IO, ba) → new_sequence(vx31, ty_IO, ba)
R is empty.
The set Q consists of the following terms:
new_gtGtEs1(:(x0, x1), x2, x3)
new_gtGtEs2(:(x0, x1), x2, x3)
new_psPs5(x0, x1, x2, x3, x4)
new_psPs2(x0, x1, x2, x3)
new_gtGtEs2([], x0, x1)
new_psPs3(:(x0, x1), x2, x3, x4)
new_psPs4(:(x0, x1), x2, x3)
new_psPs3([], x0, x1, x2)
new_gtGtEs1([], x0, x1)
new_psPs1(x0, x1)
new_psPs4([], x0, x1)
We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.
new_gtGtEs1(:(x0, x1), x2, x3)
new_gtGtEs2(:(x0, x1), x2, x3)
new_psPs5(x0, x1, x2, x3, x4)
new_psPs2(x0, x1, x2, x3)
new_gtGtEs2([], x0, x1)
new_psPs3(:(x0, x1), x2, x3, x4)
new_psPs4(:(x0, x1), x2, x3)
new_psPs3([], x0, x1, x2)
new_gtGtEs1([], x0, x1)
new_psPs1(x0, x1)
new_psPs4([], x0, x1)
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_sequence(:(vx30, vx31), ty_IO, ba) → new_sequence(vx31, ty_IO, ba)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_sequence(:(vx30, vx31), ty_IO, ba) → new_sequence(vx31, ty_IO, ba)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
Q DP problem:
The TRS P consists of the following rules:
new_gtGtEs0(:(vx300, vx301), vx31, ba) → new_psPs0(vx31, vx300, new_gtGtEs1(vx301, vx31, ba), ba)
new_psPs0(vx31, vx300, vx4, ba) → new_sequence(vx31, ty_[], ba)
new_sequence(:(:(vx300, vx301), vx31), ty_[], ba) → new_gtGtEs0(vx301, vx31, ba)
new_gtGtEs0(:(vx300, vx301), vx31, ba) → new_gtGtEs0(vx301, vx31, ba)
new_sequence(:(:(vx300, vx301), vx31), ty_[], ba) → new_psPs0(vx31, vx300, new_gtGtEs1(vx301, vx31, ba), ba)
The TRS R consists of the following rules:
new_psPs4([], vx4, ba) → vx4
new_gtGtEs1([], vx31, ba) → []
new_psPs2(vx31, vx300, vx4, ba) → new_psPs3(new_sequence0(vx31, ty_[], ba), vx300, vx4, ba)
new_psPs3([], vx300, vx4, ba) → new_psPs1(vx4, ba)
new_psPs1(vx4, ba) → vx4
new_psPs5(vx300, vx60, vx9, vx4, ba) → :(:(vx300, vx60), new_psPs4(vx9, vx4, ba))
new_gtGtEs2([], vx300, ba) → []
new_gtGtEs2(:(vx610, vx611), vx300, ba) → new_psPs4(:(:(vx300, vx610), []), new_gtGtEs2(vx611, vx300, ba), ba)
new_psPs4(:(vx90, vx91), vx4, ba) → :(vx90, new_psPs4(vx91, vx4, ba))
new_psPs3(:(vx60, vx61), vx300, vx4, ba) → new_psPs5(vx300, vx60, new_psPs1(new_gtGtEs2(vx61, vx300, ba), ba), vx4, ba)
new_gtGtEs1(:(vx300, vx301), vx31, ba) → new_psPs2(vx31, vx300, new_gtGtEs1(vx301, vx31, ba), ba)
The set Q consists of the following terms:
new_gtGtEs1(:(x0, x1), x2, x3)
new_gtGtEs2(:(x0, x1), x2, x3)
new_psPs5(x0, x1, x2, x3, x4)
new_psPs2(x0, x1, x2, x3)
new_gtGtEs2([], x0, x1)
new_psPs3(:(x0, x1), x2, x3, x4)
new_psPs4(:(x0, x1), x2, x3)
new_psPs3([], x0, x1, x2)
new_gtGtEs1([], x0, x1)
new_psPs1(x0, x1)
new_psPs4([], x0, x1)
We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
Q DP problem:
The TRS P consists of the following rules:
new_gtGtEs0(:(vx300, vx301), vx31, ba) → new_psPs0(vx31, vx300, new_gtGtEs1(vx301, vx31, ba), ba)
new_psPs0(vx31, vx300, vx4, ba) → new_sequence(vx31, ty_[], ba)
new_sequence(:(:(vx300, vx301), vx31), ty_[], ba) → new_gtGtEs0(vx301, vx31, ba)
new_gtGtEs0(:(vx300, vx301), vx31, ba) → new_gtGtEs0(vx301, vx31, ba)
new_sequence(:(:(vx300, vx301), vx31), ty_[], ba) → new_psPs0(vx31, vx300, new_gtGtEs1(vx301, vx31, ba), ba)
The TRS R consists of the following rules:
new_gtGtEs1([], vx31, ba) → []
new_gtGtEs1(:(vx300, vx301), vx31, ba) → new_psPs2(vx31, vx300, new_gtGtEs1(vx301, vx31, ba), ba)
new_psPs2(vx31, vx300, vx4, ba) → new_psPs3(new_sequence0(vx31, ty_[], ba), vx300, vx4, ba)
The set Q consists of the following terms:
new_gtGtEs1(:(x0, x1), x2, x3)
new_gtGtEs2(:(x0, x1), x2, x3)
new_psPs5(x0, x1, x2, x3, x4)
new_psPs2(x0, x1, x2, x3)
new_gtGtEs2([], x0, x1)
new_psPs3(:(x0, x1), x2, x3, x4)
new_psPs4(:(x0, x1), x2, x3)
new_psPs3([], x0, x1, x2)
new_gtGtEs1([], x0, x1)
new_psPs1(x0, x1)
new_psPs4([], x0, x1)
We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.
new_gtGtEs2(:(x0, x1), x2, x3)
new_psPs5(x0, x1, x2, x3, x4)
new_gtGtEs2([], x0, x1)
new_psPs4(:(x0, x1), x2, x3)
new_psPs1(x0, x1)
new_psPs4([], x0, x1)
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
Q DP problem:
The TRS P consists of the following rules:
new_gtGtEs0(:(vx300, vx301), vx31, ba) → new_psPs0(vx31, vx300, new_gtGtEs1(vx301, vx31, ba), ba)
new_psPs0(vx31, vx300, vx4, ba) → new_sequence(vx31, ty_[], ba)
new_sequence(:(:(vx300, vx301), vx31), ty_[], ba) → new_gtGtEs0(vx301, vx31, ba)
new_gtGtEs0(:(vx300, vx301), vx31, ba) → new_gtGtEs0(vx301, vx31, ba)
new_sequence(:(:(vx300, vx301), vx31), ty_[], ba) → new_psPs0(vx31, vx300, new_gtGtEs1(vx301, vx31, ba), ba)
The TRS R consists of the following rules:
new_gtGtEs1([], vx31, ba) → []
new_gtGtEs1(:(vx300, vx301), vx31, ba) → new_psPs2(vx31, vx300, new_gtGtEs1(vx301, vx31, ba), ba)
new_psPs2(vx31, vx300, vx4, ba) → new_psPs3(new_sequence0(vx31, ty_[], ba), vx300, vx4, ba)
The set Q consists of the following terms:
new_gtGtEs1(:(x0, x1), x2, x3)
new_psPs2(x0, x1, x2, x3)
new_psPs3(:(x0, x1), x2, x3, x4)
new_psPs3([], x0, x1, x2)
new_gtGtEs1([], x0, x1)
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_psPs0(vx31, vx300, vx4, ba) → new_sequence(vx31, ty_[], ba)
The graph contains the following edges 1 >= 1, 4 >= 3
- new_sequence(:(:(vx300, vx301), vx31), ty_[], ba) → new_gtGtEs0(vx301, vx31, ba)
The graph contains the following edges 1 > 1, 1 > 2, 3 >= 3
- new_gtGtEs0(:(vx300, vx301), vx31, ba) → new_gtGtEs0(vx301, vx31, ba)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3
- new_sequence(:(:(vx300, vx301), vx31), ty_[], ba) → new_psPs0(vx31, vx300, new_gtGtEs1(vx301, vx31, ba), ba)
The graph contains the following edges 1 > 1, 1 > 2, 3 >= 4
- new_gtGtEs0(:(vx300, vx301), vx31, ba) → new_psPs0(vx31, vx300, new_gtGtEs1(vx301, vx31, ba), ba)
The graph contains the following edges 2 >= 1, 1 > 2, 3 >= 4